-- -*-Haskell-*-

{-
 * Copyright (c) 2007 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

-- Usage:
--
--  Set up the environment
--     setenv LD_LIBRARY_PATH /opt/exp/gnu/lib:$LD_LIBRARY_PATH
--     setenv PATH /home/ggreif/%NoBackup%/Omega1.4.1:$PATH
--
--  Start the omega interpreter by typing
--     omega Thrist.omg
--  and run your commands on the prompt
--

import "LangPrelude.prg" 
  (head,tail,lookup,member,fst,snd,map,Monad,maybeM,id,ioM,Row,HasType,RCons,RNil,Eq,Equal,
  listM)

kind Doe = Wi | So

data DooBiDoo :: Doe ~> Doe ~> *0 where
  ToWi :: DooBiDoo a Wi
  SoToWi :: DooBiDoo So Wi
  WiToWi :: DooBiDoo Wi Wi
  WiToSo :: DooBiDoo Wi So
  SoTo :: DooBiDoo So b
  ToSo :: DooBiDoo a So

data ShuBiDoo :: Doe ~> Doe ~> *0 where
  WiTo :: ShuBiDoo Wi a

--$   @Definition { A @I thrist is a list-like datastructure
--$ with three type indices. It enforces the invariants that
--$ @List { @Item { it can only contain members of the same type with two type indices
--$ and } @Item { that the type indices of consequtive members must match
--$ up in the specific manner that the second type index of the
--$ left member must equal the first type index of the right one. } } }

--{
data Thrist :: forall (l :: *1) . (l ~> l ~> *)  ~> l ~> l ~> * where
  Nil :: Thrist k a a
  Cons :: k c b -> Thrist k b a -> Thrist k c a
 deriving List(l)
--}

--$   @Note { The name thrist is a portmanteau of thread and list
--$ conveying the essence of a list where the members' types are
--$ threaded up. }

{--@
By means of the @Code { deriving List(l) } declaration
we specified that thrists can be entered in @Omega using
special syntax, making it amenable to reading from the
listener, pattern matching and outputting.
@P The following example session demonstrates this:
--@-}

{- Example session:

prompt> #[]l
 #[]l : forall (a:*1) (b:a ~> a ~> *0) (c:a:*1).Thrist b c c
prompt> #[ToWi]l
 #[ToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> #[ToWi,WiToWi]l
 #[ToWi,WiToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> #[ToWi,WiToWi,ToSo]l
 #[ToWi,WiToWi,ToSo]l : forall (a:Doe).Thrist DooBiDoo a So
prompt> #[ToWi,WiToWi,ToSo,SoTo]l
 #[ToWi,WiToWi,ToSo,SoTo]l : forall (a:Doe) (b:Doe).Thrist DooBiDoo a b
prompt> #[ToWi, WiTo]l
 In the expression: Cons WiTo Nil
 the result type: Thrist ShuBiDoo Wi b
 was not what was expected: Thrist DooBiDoo Wi a

-}

##test "different constants: SchubiDoo   !=   DooBiDoo"
 fail0 = #[ToWi, WiTo]l

cat :: Thrist DooBiDoo a b -> String
cat Nil = ""
cat (Cons ToWi r) = "ToWi " ++ cat r
cat (Cons WiToWi r) = "WiToWi " ++ cat r
cat (Cons WiToSo r) = "WiToSo " ++ cat r
cat (Cons SoTo r) = "SoTo " ++ cat r
cat (Cons ToSo r) = "ToSo " ++ cat r


-- Cat thrist
-- See: http://en.wikipedia.org/wiki/Cat_%28programming_language%29

blow :: Nat ~> Row *0 ~> Row *0
{blow Z s} = s
{blow (S n) s} = RCons t {blow n s}

kind CatShape = Shape (Row *0)

data Cat :: CatShape ~> CatShape ~> *0 where
  Push :: a -> Cat (Shape s) (Shape (RCons a s))
  Dup :: Cat (Shape (RCons t s)) (Shape (RCons t (RCons t s)))
--  Dig :: Pick Row Nat -> Cat (Shape (RCons t s)) (Shape (RCons t (RCons t s)))
  Print :: Cat (Shape (RCons t s)) (Shape s)
  PopN :: Nat' (S n) -> Cat (Shape {blow (S n) s}) (Shape s)
  Swap :: Cat (Shape (RCons a (RCons b s))) (Shape (RCons b (RCons a s)))
-- Perm :: Pick Row Nat -- TODO
  Add :: Cat (Shape (RCons Int (RCons Int s))) (Shape (RCons Int s))
  Greater :: Cat (Shape (RCons Int (RCons Int s))) (Shape (RCons Bool s))
  If :: Thrist Cat (Shape s) (Shape t) ->
        Thrist Cat (Shape s) (Shape t) ->
        Cat (Shape (RCons Bool s)) (Shape t)

te1 = #[Push 42, Dup, Greater, If #[pop, Push `hh]l #[Push 42, Add, Print, Push `hh]l]l

{- This needs more magic:
showThrist :: (t a b -> String) -> Thrist t a b -> String
showThrist f Nil = ""
showThrist f (Cons t r) = f t ++ showThrist f r
-}

cat' :: Thrist Cat a b -> String
cat' Nil = ""
cat' (Cons (Push a) r) = "Push " ++ show a ++ "\n" ++ cat' r
cat' (Cons Dup r) = "Dup" ++ "\n" ++ cat' r
cat' (Cons Print r) = "Print" ++ "\n" ++ cat' r
cat' (Cons (PopN n) r) = "PopN " ++ show n ++ "\n" ++ cat' r
cat' (Cons Swap r) = "Swap" ++ "\n" ++ cat' r
cat' (Cons Add r) = "Add" ++ "\n" ++ cat' r
cat' (Cons Greater r) = "Greater" ++ "\n" ++ cat' r
cat' (Cons (If yes no) r) = "If " ++ show yes ++ " ELSE " ++ show no ++ "\n" ++ cat' r

data Stack :: Row *0 ~> *0 where
  Empty :: Stack RNil
  Pu :: a -> Stack s -> Stack (RCons a s)

interpretCat :: (forall a . Thrist Cat (Shape a) (Shape a)) -> IO (Stack RNil)
interpretCat thr = interpretCat' thr (returnIO Empty)

interpretCat' :: Thrist Cat (Shape a) (Shape b) -> IO (Stack a) -> IO (Stack b)

interpretCat' Nil act = act

interpretCat' thr act =
    case thr of
	     (Cons (Push a) r) -> do
				  st <- act
				  interpretCat' r (return (Pu a st))
	     (Cons (PopN (S n)) r) -> do
				      Pu _ st <- act
				      interpretCat' r (popMore n st)
	     (Cons Print r) -> do
			       Pu a st <- act
			       new <- putStr (show a)
			       interpretCat' r (return st)
	     (Cons Dup r) -> do
			     Pu a st <- act
  			     interpretCat' r (return (Pu a (Pu a st)))
	     (Cons Swap r) -> do
			      Pu a st <- act
			      let (Pu b st') = st
			      interpretCat' r (return (Pu b (Pu a st')))
	     (Cons Add r) -> do
			     Pu a st <- act
			     let (Pu b st') = st
			     interpretCat' r (return (Pu (a + b) st'))
	     (Cons Greater r) -> do
				 Pu a st <- act
				 let (Pu b st') = st
				 interpretCat' r (return (Pu (b > a) st'))
	     (Cons (If yes no) r) -> do
				     Pu cond st <- act
				     let act' = return st
				     interpretCat' r (if cond then interpretCat' yes act' else interpretCat' no act')
      where monad ioM

pop = PopN #1

popMore :: Nat' n -> Stack {blow n b} -> IO (Stack b)
popMore Z st = return st
    where monad ioM
popMore (S n) st = do
		   let (Pu _ st') = st
		   popMore n st'
    where monad ioM

##test "was not what was expected"
  te2 = interpretCat (Cons (Push 11) te1)

te3 = interpretCat #[Push 23, pop]l
te4 = interpretCat #[Push 42, Push 11, Greater, If #[Push True]l #[Push False]l, Print]l
te5 = interpretCat #[Push 42, Push 32, Push 1, Add, Swap, Print, Print]l
te6 = interpretCat #[Push 42, Push 32, Push 1, Add, Swap, Print, Dup, PopN #2]l

##test "Mixup in Decs (not reported yet)"
 Weee :: CatShape
 type Weee = Shape (Row *0)



--$ @Section { Crazy uses of Thrists }
--$ For example we can put functions of type
--$ a->b, b->c into a thrist:

--{
funThrist = #[ord, (+) 2, chr]l

runThrist :: Thrist (->) a b -> a -> b
runThrist Nil b = b
runThrist (Cons f r) a = runThrist r (f a)
--}

{-
-- Example session:

prompt> funThrist
 #[<primfun to1>,<fn>,<primfun to1>]l : Thrist (->) Char Char
prompt> runThrist funThrist
 <fn> : Char -> Char
prompt> runThrist funThrist 'x'
 'z' : Char

-}

--$ @Item { An interesting use are @Code { Equal } thrists
--$ as they can express transitivity relationships of
--$ type equality: @Code { Equal a b /\ Equal b c ==> Equal c a }

plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}

plusZ :: Nat' n -> Equal {plus n Z} n
plusZ Z = Eq
plusZ (S n) = Eq -- :: Equal {plus (S n) Z} (S n) -- reduces to Equal (S {plus n Z}) (S n)
  where theorem because = plusZ n -- :: Equal {plus n Z} n


plusS :: Nat' n -> Equal {plus n (S m)} (S {plus n m})
plusS Z = Eq :: Equal {plus Z (S m)} (S {plus Z m}) --> Equal (S m) (S {plus Z m}) --> Equal m {plus Z m} --> Equal m m
plusS (S n) = Eq --::  Equal {plus (S n) (S m)} (S {plus (S n) m})
                   --> Equal (S {plus n (S m)}) (S (S {plus n m}))
                   --% Equal    {plus n (S m)}     (S {plus n m})
    where theorem because = plusS n


plusCommutes :: Nat' n -> Nat' m -> Equal {plus n m} {plus m n}
plusCommutes Z m = Eq --:: Equal {plus Z m} {plus m Z}
                      -->  Equal m {plus m Z}
    where theorem because = plusZ m

plusCommutes (S n) m = Eq --:: Equal {plus (S n) m} {plus m (S n)}
                          -->  Equal (S {plus n m}) {plus m (S n)}
                          --%  Equal (S {plus n m}) (S {plus m n})
                          --%  Equal    {plus n m}     {plus m n}
    where theorem because1 = plusS m, because2 = plusCommutes n m

impliesZero :: Nat' n -> Nat' m -> Equal {plus n m} m -> Equal m Z
impliesZero Z m Eq = Eq --? Equal {plus Z m} m -> Equal m Z
                        --> Equal m m -> Equal m Z






--$ I am writing this as an equivalent thrist now


{-
hyp1 :: Nat' a -> Nat' (S b) -> Equal a (S b)
hyp1 #1 #1 = Eq
hyp1 (S a) (S b) = Eq
  where theorem because = hyp1 a b
-}

##test "Does not work yet"
 eqThrist = #[Eq :: Equal a (S b)
           , Eq :: Equal (S b) (S c)
           , Eq :: (S c) a
           ]l
